Inference at * 1 2 
Iof proof for Lemma absval lbound:

.....falsecase..... NILNIL

1. i : 
2. n : 
3. i < 0
  ((-i) > n)  ((i < (-n))  (i > n)) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)
 b

latex

 .

Definitions	, t  T, P  Q, P  Q, P & Q, P  Q, i > j, P  Q, x:A. B(x),
Lemmas	gt wf